COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	equal.lsp[s84,jmc]	Circumscribing equality
C00008 00003	labels: SIMPINFO 
C00013 00004	(proof lesseq)
C00014 ENDMK
C⊗;
;equal.lsp[s84,jmc]	Circumscribing equality

(proof equal)

(axiom |index a = 1 ∧ index b = 2 ∧ index c = 3 ∧ index d = 4|)
(label simpinfo)

(axiom |¬(1=2) ∧ ¬(1=3) ∧ ¬(2=3) ∧ ¬(1=4) ∧ ¬(2=4) ∧ ¬(2=4)|)
(label simpinfo)
; This axiom is to be removed when facilities for attachment become
; available so all such facts are directly computed by EKL.

(define equiv |∀e.equiv e ≡ (∀x.e(x,x)) ∧ (∀x y.e(x,y) ⊃ e(y,x))
	∧ (∀x y z.e(x,y) ∧ e(y,z) ⊃ e(x,z))|)

;e(x,y) is our imitation equality.

(define world1 |∀e.world1 e ≡ e(a,b) ∧ equiv e|)

(define world2 |∀e.world2 e ≡ (e(a,b) ∨ e(a,c)) ∧ equiv e|)

(define world11 |∀e.world11 e ≡ world1 e ∧ ∀e1.(world1 e1 ∧ (∀x y.e1(x,y) ⊃ e(x,y))
	⊃ (∀x y.e(x,y) ≡ e1(x,y)))|)

(define world21
	|∀e.world21 e ≡ world2 e ∧ ∀e1.(world2 e1 ∧ (∀x y.e1(x,y) ⊃ e(x,y))
	⊃ (∀x y.e(x,y) ≡ e1(x,y)))|)

8. (assume |world11(e0)|)
(define e11 |∀x y.e11(x,y) ≡ x = a ∧ y = b ∨ x = y|)

(define e21 |∀x y.e21(x,y) ≡ x = a ∧ y = b ∨ x = y|)
(define e22 |∀x y.e22(x,y) ≡ x = a ∧ y = c ∨ x = y|)

(der |equiv e11| nil (open equiv) (open e11))
(der |equiv e21| nil (open equiv) (open e21))
14. (der |equiv e22| nil (open equiv) (open e22))

15. (der |world1 e11| (12) (open world1) (open e11))

16. (der |world2 e21| (13) (open world2) (open e21))

17. (der |world2 e22| (14) (open world2) (open e22))

18. (rw 8 (open world11))

19. (der equal#18#1 18)

20. (rw 19 (open world1))

21. (rw 20 (open equiv))

22. (der |∀x y.e11(x,y) ⊃ e0(x,y)| (20 21) (open e11))

23. (der equal#18#2 18)

24. (ue ((e1.e11)) 23)

25. (der |∀x y.e0(x,y) ≡ e11(x,y)| (15 22 24))

26. (rw 25 (open e11))

27. (der |e0(a,b)| 26)

28. (der |¬(a=c)| (1 2))

29. (der |¬(b=c)| (1 2))

30. (der |¬e0(a,c)| (26 28 29))

(assume |world21 e0|)

(rw 31 (open world21))

(der equal#32#1 32)

34. (der equal#32#2 32)

(rw 33 (open world2))
;labels: SIMPINFO 
1. (AXIOM |INDEX(A)=1∧INDEX(B)=2∧INDEX(C)=3∧INDEX(D)=4|)

;labels: SIMPINFO 
2. (AXIOM |¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬2=4|)

3. (DEFINE EQUIV
     |∀E.EQUIV(E)≡
         (∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))| 
NIL)

4. (DEFINE WORLD1 |∀E.WORLD1(E)≡E(A,B)∧EQUIV(E)| NIL)

5. (DEFINE WORLD2 |∀E.WORLD2(E)≡(E(A,B)∨E(A,C))∧EQUIV(E)| NIL)

6. (DEFINE WORLD11
     |∀E.WORLD11(E)≡
         WORLD1(E)∧(∀E1.WORLD1(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))|
     NIL)

7. (DEFINE WORLD21
     |∀E.WORLD21(E)≡
         WORLD2(E)∧(∀E1.WORLD2(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))|
     NIL)

8. (ASSUME |WORLD11(E0)|)
deps: (8)

9. (DEFINE E11 |∀X Y.E11(X,Y)≡X=A∧Y=B∨X=Y| NIL)

10. (DEFINE E21 |∀X Y.E21(X,Y)≡X=A∧Y=B∨X=Y| NIL)

11. (DEFINE E22 |∀X Y.E22(X,Y)≡X=A∧Y=C∨X=Y| NIL)

12. (DERIVE |EQUIV(E11)| (NIL) ((OPEN EQUIV) (OPEN E11)))
EQUIV(E11)

13. (DERIVE |EQUIV(E21)| (NIL) ((OPEN EQUIV) (OPEN E21)))
EQUIV(E21)

14. (DERIVE |EQUIV(E22)| (NIL) ((OPEN EQUIV) (OPEN E22)))
EQUIV(E22)

15. (DERIVE |WORLD1(E11)| (12) ((OPEN WORLD1) (OPEN E11)))
WORLD1(E11)

16. (DERIVE |WORLD2(E21)| (13) ((OPEN WORLD2) (OPEN E21)))
WORLD2(E21)

17. (DERIVE |WORLD2(E22)| (14) ((OPEN WORLD2) (OPEN E22)))
WORLD2(E22)

18. (RW 8 (OPEN WORLD11))
WORLD1(E0)∧(∀E1.WORLD1(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
deps: (8)

19. (DERIVE |WORLD1(E0)| (18) NIL)
WORLD1(E0)
deps: (8)

20. (RW 19 (OPEN WORLD1))
E0(A,B)∧EQUIV(E0)
deps: (8)

21. (RW 20 (OPEN EQUIV))
E0(A,B)∧(∀X.E0(X,X))∧(∀X Y.E0(X,Y)⊃E0(Y,X))∧(∀X Y Z.E0(X,Y)∧E0(Y,Z)⊃E0(X,Z))
deps: (8)

22. (DERIVE |∀X Y.E11(X,Y)⊃E0(X,Y)| (20 21) (OPEN E11))
∀X Y.E11(X,Y)⊃E0(X,Y)
deps: (8)

23. (DERIVE |∀E1.WORLD1(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))| 
(18)
      NIL)
∀E1.WORLD1(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))
deps: (8)

24. (UE ((E1.|E11|)) 23 NIL)
WORLD1(E11)∧(∀X Y.E11(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E11(X,Y))
deps: (8)

25. (DERIVE |∀X Y.E0(X,Y)≡E11(X,Y)| (15 22 24) NIL)
∀X Y.E0(X,Y)≡E11(X,Y)
deps: (8)

26. (RW 25 (OPEN E11))
∀X Y.E0(X,Y)≡X=A∧Y=B∨X=Y
deps: (8)

27. (DERIVE |E0(A,B)| (26) NIL)
E0(A,B)
deps: (8)

28. (DERIVE |¬A=C| (SIMPINFO) NIL)
¬A=C

29. (DERIVE |¬B=C| (SIMPINFO) NIL)
¬B=C

30. (DERIVE |¬E0(A,C)| (26 28 29) NIL)
¬E0(A,C)
deps: (8)

31. (ASSUME |WORLD21(E0)|)
deps: (31)

32. (RW 31 (OPEN WORLD21))
WORLD2(E0)∧(∀E1.WORLD2(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
deps: (31)

33. (DERIVE |WORLD2(E0)| (32) NIL)
WORLD2(E0)
deps: (31)

34. (DERIVE |∀E1.WORLD2(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))| 
(32)
      NIL)
∀E1.WORLD2(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))
deps: (31)

35. (RW 33 (OPEN WORLD2))
(E0(A,B)∨E0(A,C))∧EQUIV(E0)
deps: (31)

36. 
(proof lesseq)
(decl lessp (type: |ground⊗ground→truthval|) (syntype: constant)
(infixname: <) (bindingpower: 850))
(axiom |∀x y. x < y ⊃ ¬(x = y)|)
(axiom |∀x y z. x < y ∧ y < z ⊃ x < z|)
(axiom |a < b ∧ b < c|)
(der |a < c| (2:4))
(der |a ≠ c| (2 5))
(der |a ≠ b| (2 2 4))
What about allowing the user to request DER to try harder by doubling
a premiss?  This would be analogous to the fact that DER can prove
(der |∃x.∀y.(p x ⊃ p y) ∨ ∃x.∀y.(p x ⊃ p y)|)